g, h:GrpSig, f:MonHom(g,h). IsMonHom{g,h}(f) 

latex

Up	groups 1
Definitions of Statement	IsMonHom{M1,M2}(f), MonHom(M1,M2)
Definitions	FunThru2op(A;B;opa;opb;f), IsMonHom{M1,M2}(f), MonHom(M1,M2), True, T, x. t(x), t  T, , x f y, P & Q, x:A. B(x), x(s), P  Q, SqStable(P)
Lemmas	grp sig wf, grp id wf, sq stable equal, sq stable all, grp op wf, grp car wf, sq stable and